class Frame:
    def __init__(self, levels=[{}]):
        self.levels = levels

    def lookup_binds(self, var):
        for binds in self.levels:
            if var in binds:
                return binds
        return False

    def lookup(self, var):
        binds = self.lookup_binds(var)
        if binds is not False:
            return binds[var]
        return False
        

    def copy(self):
        new_levels = []
        for binds in self.levels:
            new_levels.append(binds.copy())
        return Frame(new_levels)

    def deepen(self):
        self.levels.append({})

    def get_levels(self):
        return self.levels

    def set_var(self, var, val):
        binds = self.lookup_binds(var)
        if binds is not False:
            binds[var] = val
        self.levels[-1][var] = val

    def all_same(var, new_val):
        old_val = frame.lookup(var)
        for binds in self.levels:
            for key in binds.keys():
                if binds[key] == old_val:
                    binds[key] = new_val

def val_is_var(val):
    return type(val) is str and val[0].isupper()

def val_is_const(val):
    return type(val) is str and val[0].islower()

def val_is_fake(val):
    return type(val) is str and val[0] == '_'

fake_var_cnt = 0
def fake_var():
    global fake_var_cnt
    var = '_' + str(fake_var_cnt)
    fake_var_cnt += 1
    return var                

def unify_var(var, val, frame):
    if not val_is_var(val): # val is not a variable, either constant or complex
        if frame.lookup(var) is False: # var is not set
            frame.set_var(var, val)
            return True
        if val_is_fake(frame.lookup(var)): # var set to a fake variable
            frame.all_same(var, val) # set fake variable to val
            return True
        return unify(frame.lookup(var), val, frame) # var refers to something else, unify

    if frame.lookup(val) is False: # val is not set
        if frame.lookup(var) is False: # var is not set
            fake = fake_var()
            frame.set_var(val, fake)
            frame.set_var(var, fake) # set both to same fake variable
            return True
        frame.set_var(val, frame.lookup(var)) # set val to var, doesn't matter what var is
        return True

    if val_is_fake(frame.lookup(val)): # val refers to fake variable
        if frame.lookup(var) is False: # var is not set
            frame.set_var(var, frame.lookup(val)) # set var to fake variable
            return True
        frame.all_same(val, frame.lookup(var)) # set fake variable to var
        return True

    return unify(frame.lookup(var), frame.lookup(val), frame) #see if compatable

# sees if two things could be made the same, and if so, how.
def unify(val1, val2, frame):
    #constants
    if val_is_const(val1)  and val_is_const(val2):
        return val1 == val2

    #variables
    if val_is_var(val1):
        return unify_var(val1, val2, frame)
    if val_is_var(val2):
        return unify_var(val2, val1, frame)

    #lists
    if type(val1) is not list or type(val2) is not list:
        return False
    if len(val1) != len(val2):
        return False
    for new_val1, new_val2 in zip(val1, val2):
        if not unify(new_val1, new_val2, frame):
            return False
    return True

# table = {}
frame = Frame()

if (unify(['man', 'X', 'h'], ['man', 'socrates', 'H'], frame)):
    print(frame.get_levels())
    print('yes')
else:
    print('no')

# class Pbody:
#     def __init__(self, base, body, frame):
#         self.body = body
#         self.stack = [Pbox(base, body[0], frame)]

#     def call(self, base):
#         while True:
#             new_frame = self.stack[-1].call(base)
#             if new_frame is False:
#                 self.stack.pop()
#                 if len(self.stack) == 0:
#                     return False
#             elif len(self.stack) == len(self.body):
#                 return new_frame
#             else:
#                 stack.append(Pbox(base, body[len(self.stack)], new_frame))
                

# class Pbox:
#     def __init__(self, base, q, frame=Frame()):
#         self.iterator = iter(base)
#         self.q = q
#         self.frame = frame
#         self.body = None

#     def call(self, base):
#         if self.body is not None:
#             body_frame = self.body.call(base)
#             if body_frame is not False:
#                 return body_frame
#             self.body = None

#         for fact in self.iterator:
#             new_frame = self.frame.copy()
#             new_frame.deepen()
#             if unify(self.q, fact[0], new_frame):
#                 new_body = fact[1]
#                 if len(new_body) == 0:
#                     return new_frame
#                 pbody = Pbody(base, new_body, new_frame)
#                 final_frame = pbody.call(base)
#                 if final_frame is not False:
#                     self.body = pbody
#                     return final_frame
#         return False
                
# base = [
#     # [['true', 'True'],     []             ],
#     [['human', 'X'],         [['man', 'X']]   ],
#     [['man', 'socrates'],  []             ],
#     [['woman', 'ophelia'], []             ],
#     [['human', 'Y'],         [['woman', 'Y']] ],
#     [['mortal', 'Z'],        [['human', 'Z']] ]
# ]

# box = Pbox(base, ['A', 'socrates'])

# # frame = box.call(base)
# # if frame is not False:
# #     print(frame.get_levels())
# # else:
# #     print('no')
    
# frame = box.call(base)
# while frame is not False:
#     print(frame.get_levels())
#     frame = box.call(base)

# # frame = Frame()
# # unify(['mortal', 'socrates'], ['mortal', 'X'], frame)
# # print(frame.get_levels())
